Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)

Q is empty.


↳ QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

IF_97(st_1, in_2, st_2, in_3, st_3, m, true) -> RING6(st_1, in_2, st_2, tail1(in_3), st_3, m)
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> HEAD1(in_2)
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> TAIL1(in_3)
IF_37(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, st_2)
IF_97(st_1, in_2, st_2, in_3, st_3, m, true) -> TAIL1(in_3)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> HEAD1(in_3)
SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> MAP_F2(two, head1(in_2))
IF_57(st_1, in_2, st_2, in_3, st_3, m, true) -> RING6(st_1, tail1(in_2), st_2, in_3, st_3, m)
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> IF_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, app2(map_f2(three, head1(in_3)), st_3))
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> APP2(map_f2(two, head1(in_2)), st_2)
IF_77(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
IF_57(st_1, in_2, st_2, in_3, st_3, m, true) -> TAIL1(in_2)
IF_37(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> APP2(map_f2(three, head1(in_3)), st_3)
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, app2(map_f2(two, head1(in_2)), st_2))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> MAP_F2(two, head1(in_2))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> LENGTH1(st_2)
IF_27(st_1, in_2, st_2, in_3, st_3, m, true) -> EMPTY1(fstsplit2(m, st_2))
APP2(cons2(h, t), x) -> APP2(t, x)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> EMPTY1(map_f2(two, head1(in_2)))
LENGTH1(cons2(h, t)) -> LENGTH1(t)
IF_17(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, st_1)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> HEAD1(in_3)
IF_67(st_1, in_2, st_2, in_3, st_3, m, true) -> EMPTY1(fstsplit2(m, st_3))
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> IF_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, app2(map_f2(two, head1(in_2)), st_2))
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> EMPTY1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3)))
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> MAP_F2(two, head1(in_2))
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> APP2(map_f2(three, head1(in_3)), st_3)
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> HEAD1(in_3)
IF_27(st_1, in_2, st_2, in_3, st_3, m, true) -> IF_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
IF_37(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, st_2)
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> MAP_F2(three, head1(in_3))
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, app2(map_f2(two, head1(in_2)), st_2))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> LEQ2(m, length1(st_3))
IF_77(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, st_3)
MAP_F2(pid, cons2(h, t)) -> APP2(f2(pid, h), map_f2(pid, t))
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> HEAD1(in_2)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> LEQ2(m, length1(st_2))
IF_17(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
IF_27(st_1, in_2, st_2, in_3, st_3, m, true) -> FSTSPLIT2(m, st_2)
IF_67(st_1, in_2, st_2, in_3, st_3, m, true) -> FSTSPLIT2(m, st_3)
FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> LENGTH1(st_3)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> MAP_F2(three, head1(in_3))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> EMPTY1(map_f2(three, head1(in_3)))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> EMPTY1(fstsplit2(m, st_1))
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> TAIL1(in_2)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> HEAD1(in_2)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
IF_17(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, st_1)
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> MAP_F2(three, head1(in_3))
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> EMPTY1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, app2(map_f2(three, head1(in_3)), st_3))
LEQ2(s1(n), s1(m)) -> LEQ2(n, m)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> FSTSPLIT2(m, st_1)
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> APP2(map_f2(two, head1(in_2)), st_2)
IF_67(st_1, in_2, st_2, in_3, st_3, m, true) -> IF_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

IF_97(st_1, in_2, st_2, in_3, st_3, m, true) -> RING6(st_1, in_2, st_2, tail1(in_3), st_3, m)
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> HEAD1(in_2)
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> TAIL1(in_3)
IF_37(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, st_2)
IF_97(st_1, in_2, st_2, in_3, st_3, m, true) -> TAIL1(in_3)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> HEAD1(in_3)
SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> MAP_F2(two, head1(in_2))
IF_57(st_1, in_2, st_2, in_3, st_3, m, true) -> RING6(st_1, tail1(in_2), st_2, in_3, st_3, m)
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> IF_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, app2(map_f2(three, head1(in_3)), st_3))
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> APP2(map_f2(two, head1(in_2)), st_2)
IF_77(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
IF_57(st_1, in_2, st_2, in_3, st_3, m, true) -> TAIL1(in_2)
IF_37(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> APP2(map_f2(three, head1(in_3)), st_3)
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, app2(map_f2(two, head1(in_2)), st_2))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> MAP_F2(two, head1(in_2))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> LENGTH1(st_2)
IF_27(st_1, in_2, st_2, in_3, st_3, m, true) -> EMPTY1(fstsplit2(m, st_2))
APP2(cons2(h, t), x) -> APP2(t, x)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> EMPTY1(map_f2(two, head1(in_2)))
LENGTH1(cons2(h, t)) -> LENGTH1(t)
IF_17(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, st_1)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> HEAD1(in_3)
IF_67(st_1, in_2, st_2, in_3, st_3, m, true) -> EMPTY1(fstsplit2(m, st_3))
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> IF_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, app2(map_f2(two, head1(in_2)), st_2))
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> EMPTY1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3)))
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> MAP_F2(two, head1(in_2))
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> APP2(map_f2(three, head1(in_3)), st_3)
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> HEAD1(in_3)
IF_27(st_1, in_2, st_2, in_3, st_3, m, true) -> IF_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
IF_37(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, st_2)
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> MAP_F2(three, head1(in_3))
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, app2(map_f2(two, head1(in_2)), st_2))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> LEQ2(m, length1(st_3))
IF_77(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, st_3)
MAP_F2(pid, cons2(h, t)) -> APP2(f2(pid, h), map_f2(pid, t))
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> HEAD1(in_2)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> LEQ2(m, length1(st_2))
IF_17(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
IF_27(st_1, in_2, st_2, in_3, st_3, m, true) -> FSTSPLIT2(m, st_2)
IF_67(st_1, in_2, st_2, in_3, st_3, m, true) -> FSTSPLIT2(m, st_3)
FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> LENGTH1(st_3)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> MAP_F2(three, head1(in_3))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> EMPTY1(map_f2(three, head1(in_3)))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> EMPTY1(fstsplit2(m, st_1))
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> TAIL1(in_2)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> HEAD1(in_2)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
IF_17(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, st_1)
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> MAP_F2(three, head1(in_3))
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> EMPTY1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, app2(map_f2(three, head1(in_3)), st_3))
LEQ2(s1(n), s1(m)) -> LEQ2(n, m)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> FSTSPLIT2(m, st_1)
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> APP2(map_f2(two, head1(in_2)), st_2)
IF_67(st_1, in_2, st_2, in_3, st_3, m, true) -> IF_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 7 SCCs with 45 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP2(cons2(h, t), x) -> APP2(t, x)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


APP2(cons2(h, t), x) -> APP2(t, x)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( cons2(x1, x2) ) = x1 + x2 + 1


POL( APP2(x1, x2) ) = x1 + x2



The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( cons2(x1, x2) ) = x2 + 1


POL( MAP_F2(x1, x2) ) = x2



The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LENGTH1(cons2(h, t)) -> LENGTH1(t)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


LENGTH1(cons2(h, t)) -> LENGTH1(t)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( cons2(x1, x2) ) = x2 + 1


POL( LENGTH1(x1) ) = x1



The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LEQ2(s1(n), s1(m)) -> LEQ2(n, m)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


LEQ2(s1(n), s1(m)) -> LEQ2(n, m)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( s1(x1) ) = x1 + 1


POL( LEQ2(x1, x2) ) = x1



The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( SNDSPLIT2(x1, x2) ) = x1


POL( cons2(x1, x2) ) = max{0, -1}


POL( s1(x1) ) = x1 + 1



The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( cons2(x1, x2) ) = max{0, -1}


POL( s1(x1) ) = x1 + 1


POL( FSTSPLIT2(x1, x2) ) = x1



The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF_97(st_1, in_2, st_2, in_3, st_3, m, true) -> RING6(st_1, in_2, st_2, tail1(in_3), st_3, m)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
IF_57(st_1, in_2, st_2, in_3, st_3, m, true) -> RING6(st_1, tail1(in_2), st_2, in_3, st_3, m)
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> IF_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> IF_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
IF_77(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
IF_37(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
IF_17(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
IF_27(st_1, in_2, st_2, in_3, st_3, m, true) -> IF_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
IF_67(st_1, in_2, st_2, in_3, st_3, m, true) -> IF_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.